L:Dsys List. (A,BL.A || B)  (M:Dsys. (BL. M || B)  M || (L)) 

latex

Definitions	{T}, A  B, x,y. t(x;y), P  Q, (x,yL.P(x;y)), , xL. P(x), x. t(x), Prop, A || B, l[i], MsgA, Id, {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, x:A. B(x), t  T, (L), Dsys
Lemmas	dsys wf, m-sys-null-compatible-right, select wf, msga wf, Id wf, m-sys-compatible wf, int seg wf, length wf2, l all wf, dsys-compatible-join, l all cons, pairwise-cons, pairwise wf, dsys-join-list-property